the_es:event_system{i:l}.
trans(es-E(the_es); e,e'.es-locl(the_es; e; e'))
SWellFounded(es-locl(the_es; e; e'))
(e,e':es-E(the_es).
(loc(e) = loc(e') 
Id) 
(es-locl(the_es; e; e') 
(e = e') es-locl(the_es; e'; e)))
(e:es-E(the_es). (
es-first(the_es; e)) (e':es-E(the_es). 
es-locl(the_es; e'; e)))
(e:es-E(the_es).
((es-first(the_es; e)))
(es-locl(the_es; es-pred(the_es; e); e)
(e':es-E(the_es). (es-locl(the_es; es-pred(the_es; e); e') es-locl(the_es; e'; e)))))
(e:es-E(the_es).
((es-first(the_es; e)))
(x:Id, t:rationals.
es_state_when(the_es; e)(x,t)
=
es_state_after(the_es; es-pred(the_es; e))
(x
,t + (es-time(the_es; e) - es-time(the_es; es-pred(the_es; e))))
es-vartype(the_es; loc(e); x)))
trans(es-E(the_es); e,e'.es-causl(the_es; e; e'))
SWellFounded(es-causl(the_es; e; e'))
(e:es-E(the_es).
(es-isrcv(the_es; e))
(es-sends(the_es; es-lnk(the_es; e); es-sender(the_es; e))[es-index(the_es; e)]
(=
(msg(es-lnk(the_es; e); es-tag(the_es; e); es-val(the_es; e))
( es-Msg(the_es)))
(e,e':es-E(the_es). es-locl(the_es; e; e') es-causl(the_es; e; e'))
(e:es-E(the_es). (es-isrcv(the_es; e)) es-causl(the_es; es-sender(the_es; e); e))
(e,e':es-E(the_es).
es-causl(the_es; e; e')
((((es-first(the_es; e')))
c (es-causl(the_es; e; es-pred(the_es; e')) (e = es-pred(the_es; e'))))
((es-isrcv(the_es; e'))
c (es-causl(the_es; e; es-sender(the_es; e')) (e = es-sender(the_es; e'))))))
(e:es-E(the_es). (es-isrcv(the_es; e)) (loc(e) = destination(es-lnk(the_es; e)) Id))
(e:es-E(the_es), l:IdLnk.
((loc(e) = source(l) Id)) (es-sends(the_es; l; e) = [] (es-Msgl(the_es; l) List)))
(e,e':es-E(the_es).
(es-isrcv(the_es; e))
(es-isrcv(the_es; e'))
(es-lnk(the_es; e) = es-lnk(the_es; e') IdLnk)
(es-locl(the_es; e; e')
(es-locl(the_es; es-sender(the_es; e); es-sender(the_es; e'))
((es-sender(the_es; e) = es-sender(the_es; e') es-E(the_es))
(es-index(the_es; e) < es-index(the_es; e'))))))
(e:es-E(the_es), l:IdLnk, n:int_seg(0; ||es-sends(the_es; l; e)||).
e':es-E(the_es)
((es-isrcv(the_es; e'))
c ((es-lnk(the_es; e') = l)
c (es-sender(the_es; e') = e)
c (es-index(the_es; e') = n 
))))